theory Gencode imports Executable Efficient_Nat
begin

code_modulename OCaml 
  SynLang SynLangExec
  Executable SynLangExec

export_code check_program vals_tp InterTyp
  in OCaml file "gencode.ml"

end
